B:Type, P:(B). finite-type(B)  finite-type({b:B| P(b)} ) 

latex

Definitions	x:A. B(x), P  Q, x(s), x:A. B(x), , t  T, P & Q, T, True, (x  l), A c B, A  B, A, False, P  Q, P  Q, {T}, SqStable(P),
Lemmas	implies functionality wrt iff, finite-type wf, l member wf, assert wf, finite-type-iff-list, bool wf, filter type, member filter, sq stable from decidable, decidable assert, length wf1, select wf